\begin{tabbing}
pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$p$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\uparrow$($P$($x_{0}$))) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). (es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id)))\+
\\[0ex]\& (\=(es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r $X$)\+
\\[0ex]c$\wedge$ \=(alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = locl($a$) $\in$ Knd)\+
\\[0ex]$\Rightarrow$ ((es{-}valtype(${\it es}$; $e$) $\subseteq$r p{-}outcome($p$)) c$\wedge$ ($\uparrow$($P$(es{-}when(${\it es}$; $x$; $e$))))))
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.existse{-}ge(${\it es}$;$e$;${\it e'}$.(es{-}kind(${\it es}$; ${\it e'}$) = locl($a$) $\in$ Knd)\+
\\[0ex]$\vee$ ($\neg$($\uparrow$($P$(es{-}after(${\it es}$; $x$; ${\it e'}$)))))))))
\-\-\-\\[0ex]\& init{-}p(${\it es}$; $i$; $X$; $x$; $x_{0}$)
\-
\end{tabbing}